COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	samele.lsp[f85,jmc]	samelength definition and proof
C00006 ENDMK
C⊗;
;;;samele.lsp[f85,jmc]	samelength definition and proof

(defax samelength |(∀v.samelength(nil,v) ≡ null(v))
∧ (∀x u.¬samelength(x.u,nil))
∧ (∀x u y v.samelength(x.u,y.v) = samelength(u,v))|)

(define samelength |(∀v.samelength(nil,v) ≡ null(v))
∧ (∀x u.¬samelength(x.u,nil))
∧ (∀x u y v.samelength(x.u,y.v) = samelength(u,v))| (use listinductiondef))

(define samelength |(∀v.samelength(nil,v) ≡ null(v))
∧ (∀x u v.samelength(x.u,v) ≡ if null v then false
else samelength(u,cdr v))| (use listinductiondef))
(proof foo)
(get-proofs lispax prf prf jk)
;the term SAMELENGTH(X.U,V)≡(IF NULL V THEN FALSE ELSE SAMELENGTH(U,CDR 
V)) is replaced by:
IF NULL V THEN SAMELENGTH(X.U,V)≡FALSE ELSE SAMELENGTH(X.U,V)≡SAMELENGTH(U,CDR 
V)
;the term V is replaced by:
NIL
;the term SAMELENGTH(X.U,NIL)≡FALSE is replaced by:
¬SAMELENGTH(X.U,NIL)
;define: could not deduce the validity of this definition:
∃SAMELENGTH.(∀V.SAMELENGTH(NIL,V)≡NULL V)∧
            (∀X U V.(IF NULL V THEN ¬SAMELENGTH(X.U,NIL)
                        ELSE SAMELENGTH(X.U,V)≡SAMELENGTH(U,CDR V)))
;did not re-write to true.
63. 

(define samelength |(∀v.samelength(v,nil) ≡ null(v))
∧ (∀x u v.samelength(x.u,v) ≡ if null v then false
else samelength(u,cdr v))| (use listinductiondef))
;the term SAMELENGTH(X.U,V)≡(IF NULL V THEN FALSE ELSE SAMELENGTH(U,CDR 
V)) is replaced by:
IF NULL V THEN SAMELENGTH(X.U,V)≡FALSE ELSE SAMELENGTH(X.U,V)≡SAMELENGTH(U,CDR 
V)
;the term V is replaced by:
NIL
;the term SAMELENGTH(X.U,NIL) is replaced by:
NULL X.U
;the term NULL X.U is replaced by:
FALSE
;the term FALSE≡FALSE is replaced by:
¬FALSE
;the term ¬FALSE is replaced by:
TRUE
;the term IF NULL V THEN TRUE ELSE SAMELENGTH(X.U,V)≡SAMELENGTH(U,CDR V) 
is replaced by:
NULL V∨(SAMELENGTH(X.U,V)≡SAMELENGTH(U,CDR V))
;define: could not deduce the validity of this definition:
∃SAMELENGTH.(∀V.SAMELENGTH(V,NIL)≡NULL V)∧
            (∀X U V.NULL V∨(SAMELENGTH(X.U,V)≡SAMELENGTH(U,CDR V)))
;did not re-write to true.
63.